FDL - Nuprl Lemma : monot_functionality

Nuprl Lemma : monot_functionality

T:Type, R, R':(T

T

), f:(T

T).
(

x, y:T. R(x,y)

R'(x,y))

(monot(T;x,y.R(x,y);f)

monot(T;x,y.R'(x,y);f))

Up gen algebra 1

Definitions of Statement monot(T;x,y.R(x;y);f)

Definitions t T, monot(T;x,y.R(x;y);f), x(s1,s2), P Q, , x:A. B(x), P Q, P & Q, P Q

Lemmas iff wf